|
課程名稱 |
軟體規格與驗証
Software Specification and Verification |
|
開課學期 |
100-1 |
|
授課對象 |
管理學院 資訊管理學研究所 |
|
授課教師 |
蔡益坤 |
|
課號 |
IM7079 |
|
課程識別碼 |
725 U3220 |
|
班次 |
|
|
學分 |
3 |
|
全/半年 |
半年 |
|
必/選修 |
選修 |
|
上課時間 |
星期四6,7,8(13:20~16:20) |
|
上課地點 |
管二303 |
|
備註 |
本課程中文授課,使用英文教科書。
總人數上限：30人
外系人數限制：5人 |
|
|
|
|
課程簡介影片 |
|
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
|
課程大綱
|
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
|
課程概述 |
本課程為正規軟體規格與驗證之入門課程，涵蓋用於描述軟體程式性質及證明特定軟體確實滿足其性質的正規語言、方法及工具。我們將專注在演譯式的方法﹝包括定理證明﹞。另一門與本課程互補，名為「自動化軟體驗證」的課程則專注在演算式的方法﹝包括模型檢驗﹞。我們將兼顧廣度與廣度深度，不僅研習基礎的原理，也探究一些較成功的正規語言、技術及工具。 |
|
課程目標 |
使學生熟悉正規軟體驗證的基礎知識，為未來在該領域從事研究做好準備。 |
|
課程要求 |
本課程包括期末考、數次作業、及一篇期末報告。
每位同學同時必須就一個選定的主題在課堂上做口頭報告，視為期末報告之一部分。
|
|
預期每週課後學習時數 |
|
|
Office Hours |
備註： 星期三下午1:30--2:30或另行約定 |
|
指定閱讀 |
Class Notes and Selected Readings (available on the course Web site) |
|
參考書目 |
1. Logic for Computer Science, J.H. Gallier, Harper & Row Publishers, 1985.
2. Proof Theory and Automated Deduction, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
3. A Logical Approach to Discrete Math, D. Gries and F.B. Schneider, Springer-Verlag, 1993.
4. Foundations for Programming Languages, J.C. Mitchell, The MIT Press, 1996.
5. Formal Syntax and Semantics of Programming Languages, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
6. Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
7. The Science of Programming, D. Gries, Springer-Verlag, 1981.
8. Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990.
9. Programming from Specifications, 2nd Edition, C. Morgan, 1994.
10. The Z Notation: A Reference Manual, 2nd Edition, J.M. Spivey, 1992.
11. Software Engineering with B, J.B. Wordsworth, Addison-Wesley, 1996.
12. Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
13. The Temporal Logic of Reactive and Concurrent Systems: Specification, Z. Manna and A. Pnueli, Springer-Verlag, 1992.
14. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995.
15. Temporal Verification of Reactive Systems: Progress, Z. Manna and A. Pnueli, Book Draft, 1996.
16. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, L. Lamport, Addison-Wesley, 2003.
17. Parallel Program Design: A Foundation, K.M. Chandy and J. Misra, Addison-Wesley, 1988.
18. A Discipline of Multiprogramming: Programming Theory for Distributed Applications, J. Misra, Springer, 2001
19. Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra, Edited by W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, Springer-Verlag, 1990
20. The Formal Methods Page: http://vl.fmnet.info/, J. Bowen.
|
|
評量方式
(僅供參考) |
|
No. |
項目 |
百分比 |
說明 |
|
1. |
期末考 |
40% |
|
2. |
作業 |
20% |
|
3. |
期末報告 |
40% |
|
|
|
週次 |
日期 |
單元主題 |
|
第1週 |
9/15 |
Introduction, Propositional Logic |
|
第2週 |
9/22 |
First-Order Logic |
|
第3週 |
9/29 |
Logical Proofs in the Coq Proof Assistant |
|
第4週 |
10/06 |
Verification of Sequential Programs: Hoare Logic |
|
第5週 |
10/13 |
Verification of Sequential Programs: Soundness and Completeness of Hoare Logic |
|
第6週 |
10/20 |
Predicate Transformers and Program Derivation |
|
第7週 |
10/27 |
Semantic Modeling in Coq |
|
第8週 |
11/03 |
Procedures + Object Orientation |
|
第9週 |
11/10 |
Program Verification Tools: Why, Caduceus, and Krakatoa |
|
第10週 |
11/17 |
Data Refinement + Formal Methods: Z |
|
第11週 |
11/24 |
Data Refinement + Formal Methods: B |
|
第12週 |
12/01 |
Data Refinement + Formal Methods: Alloy |
|
第13週 |
12/08 |
Concurrent, Reactive Systems: Owicki-Gries Method |
|
第14週 |
12/15 |
Concurrent, Reactive Systems: UNITY, Linear Temporal Logic |
|
第15週 |
12/22 |
Selected Topics: Modular/Compositional Reasoning |
|
第16週 |
12/29 |
Final |
|
第17週 |
1/05 |
Selected Topics: Separation Logic |
|
第18週 |
1/12 |
Selected Topics: Proof-Carrying Code |
|